Nuprl Lemma : loc_wf
11,40
postcript
pdf
E
,
X1
,
X2
:Type,
info
:(
E
((
:Id
X1
) + (
:(
:IdLnk
E
)
X2
))),
e
:
E
. loc(
e
)
Id
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
loc(
e
)
,
x
.
t
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
(
s
)
,
x
(
s1
,
s2
)
Lemmas
ecase1
wf
,
Id
wf
,
ldst
wf
,
IdLnk
wf
origin
E,X1,X2:Type, info:(E
((:Id 
X1) + (:(:IdLnk E) X2))), e:E. loc(e) 
Id E,X1,X2:Type, info:(E((:Id X1) + (:(:IdLnk E) X2))), e:E. loc(e) Id x:A. B(x) T
x. t(x)x,y. t(x;y)